$\forall$$T$:Type, $a$, ${\it a'}$, $b$, ${\it b'}$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).
\\[0ex]($a$ $\Lleftarrow\!\Rrightarrow$\{$T$\} $b$) $\Rightarrow$ (${\it a'}$ $\Lleftarrow\!\Rrightarrow$\{$T$\} ${\it b'}$) $\Rightarrow$ (($a$ $\Lleftarrow\!\Rrightarrow$\{$T$\} ${\it a'}$) $\Leftarrow\!\Rightarrow$ ($b$ $\Lleftarrow\!\Rrightarrow$\{$T$\} ${\it b'}$))